Inference at * 1 0 
Iof proof for Lemma connex functionality wrt iff:



1. T : Type
2. R : TT
3. R' : TT
4. x, y:T. R(x,y)  R'(x,y)
  (x, y:T. R(x,y)  R(y,x))  (x, y:T. R'(x,y)  R'(y,x)) 

latex

 by PERMUTE{1:n,
 by PERMUTE{2:n,
 by PERMUTE{2:n,
 by PERMUTE{2:n,
 by PERMUTE{3:n,
 by PERMUTE{3:n,
 by PERMUTE{4:n,
 by PERMUTE{5:n,
 by PERMUTE{6:n,
 by PERMUTE{7:n,
 by PERMUTE{7:n,
 by PERMUTE{8:n,
 by PERMUTE{9:n,
 by PERMUTE{10:n,
 by PERMUTE{11:n,
 by PERMUTE{12:n,
 by PERMUTE{13:n,
 by PERMUTE{14:n,
 by PERMUTE{15:n,
 by PERMUTE{16:n,
 by PERMUTE{16:n,
 by PERMUTE{15:n,
 by PERMUTE{7:n,
 by PERMUTE{3:n,
 by PERMUTE{17:n,
 by PERMUTE{18:n} 

latex

 1: .....wf..... NILNIL

 1:   (x, y:T. R(x,y)  R(y,x))  
 2: .....wf..... NILNIL

 2:   (x, y:T. R'(x,y)  R'(y,x))  
 3: .....wf..... NILNIL

 3:   T  Type
 4: .....wf..... NILNIL

 4:   (x.y:T. R(x,y)  R(y,x))  T
 5: .....wf..... NILNIL

 5:   (x.y:T. R'(x,y)  R'(y,x))  T
 6: .....wf..... NILNIL

 6:   T = T
 7: .....wf..... NILNIL

 7: 5. T
 7:   T  Type
 8: .....wf..... NILNIL

 8: 5. x : T
 8:   (y.R(x,y)  R(y,x))  T
 9: .....wf..... NILNIL

 9: 5. x : T
 9:   (y.R'(x,y)  R'(y,x))  T
 10: .....wf..... NILNIL

 10: 5. T
 10:   T = T
 11: .....wf..... NILNIL

 11: 5. x : T
 11: 6. y : T
 11:   R(x,y)  
 12: .....wf..... NILNIL

 12: 5. x : T
 12: 6. y : T
 12:   R'(x,y)  
 13: .....wf..... NILNIL

 13: 5. x : T
 13: 6. y : T
 13:   R(y,x)  
 14: .....wf..... NILNIL

 14: 5. x : T
 14: 6. y : T
 14:   R'(y,x)  
 15: .....wf..... NILNIL

 15: 5. x : T
 15: 6. T
 15:   x  T
 16: .....wf..... NILNIL

 16: 5. T
 16: 6. y : T
 16:   y  T
 17: .....wf..... NILNIL

 17:   (x, y:T. R'(x,y)  R'(y,x)) = (x, y:T. R'(x,y)  R'(y,x))
 18: 

 18:   (x, y:T. R'(x,y)  R'(y,x))  (x, y:T. R'(x,y)  R'(y,x))
 .

Definitions	t  T, x:A  B(x), x.A(x), f(a), s = t, P  Q, x(s1,s2), , x:AB(x), Type, x(s), P & Q, x. t(x), P  Q, P  Q, P  Q, x:A. B(x)
Lemmas	or functionality wrt iff, all functionality wrt iff, iff functionality wrt iff